Summary

Add three semantics fixes needed by the closure-call path, plus a regression test:

• Add aggregateKindClosure reduction:
  • ARGS:List ~> #mkAggregate(aggregateKindClosure(...)) => Aggregate(variantIdx(0), ARGS)
• Add #setTupleArgs(IDX, VAL:Value) [owise] fallback for unwrapped single-value arguments
• Add typed-closure callee setup rule setupCalleeClosure3 (with isFunType predicate)
• Add closure-no-capture.rs regression test

Context

Stable MIR represents closure construction via Rvalue::Aggregate(AggregateKind::Closure(...)). The K semantics had rules for tuple/ADT aggregates, but no rule for aggregateKindClosure.

For closure calls, argument placement goes through #setTupleArgs. Existing rules only handled tuple/list-shaped payloads.

Also, once closure type metadata is present, closure env locals can be typed as Ref<FunType(...)>. Before this PR, closure setup rules only matched VoidType-based closure typing paths, so the typed closure path needed an explicit setup rule.

Red vs Green for aggregateKindClosure

RED:

ListItem(...) ~> #mkAggregate(aggregateKindClosure(...))

No matching rule, execution is stuck.

GREEN:
aggregateKindClosure reduces to Aggregate(variantIdx(0), ARGS), so closure aggregate construction proceeds.

Red vs Green for #setTupleArgs [owise]

After closure aggregate reduction is added, execution advances to the next blocker:

RED (next blocker):

#setTupleArgs(2, Integer(41,8,false))

No existing #setTupleArgs rule matches this plain Value shape.

GREEN:
The fallback

#setTupleArgs(IDX, VAL:Value) => #setLocalValue(..., #incrementRef(VAL)) [owise]

handles the unwrapped single-value case and allows argument setup to continue.

Red vs Green for setupCalleeClosure3

With typed closure metadata, closure env can appear as Ref<FunType(...)>. Existing closure setup rules were guarded for VoidType closure typing paths, so typed closure setup could miss those rules.

RED:
Typed closure env path does not satisfy the existing VoidType guard shape for closure setup, so closure-call setup does not reliably take the typed closure path.

GREEN:
setupCalleeClosure3 adds the typed path explicitly:

• guard uses isFunType(#lookupMaybeTy(pointeeTy(...)))
• still performs the same tuple-arg unpacking via #setTupleArgs(2, getValue(LOCALS, TUPLE))

This keeps closure-call argument placement consistent when closure env typing is known.

Proof evidence

Without fix (RED): closure-no-capture.rs gets stuck on closure aggregate, and after adding only the closure aggregate rule it gets stuck at #setTupleArgs(2, Integer(41,8,false)).

With fix (GREEN):

test_prove_rs[closure-no-capture] PASSED

Test plan

• test_prove_rs[closure-no-capture]
• make test-integration regression